T:Type, eq:EqDecider(T), es:ES, x:Id, e, e':{e:E| @loc(e)(x:T)} .
(lastchange(x;e) = lastchange(x;e')  E)  e''[e',e).(x after e'') = (x when e)  T 

latex

Definitions	True, T, @i(x:T), P  Q, P & Q, P  Q, , t  T, e[e1,e2).P(e), P  Q, EqDecider(T), x:A. B(x), e@i. P(e), {T}, SQType(T), SqStable(P), (e <loc e')
Lemmas	es-lc-le, es-le transitivity, es-vartype wf, sq stable subtype rel, Id sq, es-locl-iff, es-loc-pred, true wf, squash wf, es-le-loc, decidable assert, es-isconst wf, sq stable from decidable, es-lc-after, assert wf, iff wf, bool wf, event system wf, Id wf, es-loc wf, es-dtype wf, es-lc wf, es-E wf, es-le wf, es-locl wf